the_es:ES.
(Trans e,e':E. (e <loc e'))
& SWellFounded((e <loc e'))
& (e, e':E. loc(e) = loc(e')  Id  (e <loc e')  e = e'  (e' <loc e))
& (e:E. first(e)  (e':E. (e' <loc e)))
& (e:E. first(e)  (pred(e) <loc e) & (e':E. ((pred(e) <loc e') & (e' <loc e))))
& (e:E. first(e)  (x:Id. (x when e) = (x after pred(e))  vartype(loc(e);x)))
& (Trans e,e':E. (e < e'))
& SWellFounded((e < e'))
& (e:E. isrcv(e)  sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))  Msg)
& (e, e':E. (e <loc e')  (e < e'))
& (e:E. isrcv(e)  (sender(e) < e))
& (e, e':E.
& ((e < e')
& ( first(e') & (e < pred(e'))  e = pred(e')  isrcv(e') & (e < sender(e'))  e = sender(e'))
& (e:E. isrcv(e)  loc(e) = destination(lnk(e))  Id)
& (e:E, l:IdLnk. loc(e) = source(l)  Id  sends(l;e) = nil  (Msg on l) List)
& (e, e':E.
& (isrcv(e)
& ( isrcv(e')
& ( lnk(e) = lnk(e')  IdLnk
& ( ((e <loc e')
& ( (
& ( ((sender(e) <loc sender(e'))  sender(e) = sender(e')  E & index(e)<index(e')))
& (e:E, l:IdLnk, n:||sends(l;e)||.
& (e':E. isrcv(e') & lnk(e') = l & sender(e') = e & index(e') = n  ) 

latex

Definitions

x:AB(x), t  T, x. t(x), x:AB(x), Type, x,y. t(x;y), destination(l), P  Q, x:A. B(x), SESAxioms{i:l}(E; T; pred?; info; when; after), S  T, Knd, EOrderAxioms(E; pred?; info), es_info(es), es-pred?(es), E, es-M(es), es_val(es), es-Trans(es), es_init(es), es-oaxioms(es), es-eq(es), kind(e), (e < e'), loc(e), Msg, state after e, (state when e), es-T(es), index(e), sender(e), lnk(e), isrcv(e), sends(l;e), (e <loc e'), (Msg on l), pred(e), first(e), val(e), tag(e), (x after e), x when e, vartype(i;x), ES, Trans x,y:T. E(x;y), P  Q, type List, a<b, {i..j}, , <a,b>, when-after(e;info;pred?;init;Trans;val), 2of(t), s.x, x.A(x), 1of(t), f(a), kindcase(k; a.f(a); l,t.g(l;t) ), pred(e), loc(e), s = t, Id, x:A. B(x), first(e), b, A, P  Q, e < e', sender(e), link(e), IdLnk, rcv?(e), source(l), P & Q, pred!(e;e'), SWellFounded(R(x;y)), Unit, left+right, A & B, {T}, SQType(T), Prop, s ~ t, Atom$n, let x = a in b(x), b, , False, ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), , {x:A| B(x) }, P  Q, kind(e), lnk(k), True, T, Void, isrcv(k), Msg(M), tag(k), islocal(k), rcv(l,tg), sends(dE;dL;pred?;info;val;p;e;l), l[i], Msg_sub(l;M), haslink(l;m), x f y, i=j, rel_exp(T;R;n), , R^+, #$n, index(dE;dL;pred?;info;p;r), AB, i  j < k, IdLnkDeq, receives(dE;dL;pred?;info;p;e;l), rcv-from-on(dE;dL;info;e;l;r), ||as||, Dec(P), x:A. B(x), Top, nil

Lemmas

IdLnk sq, rcv?-link, length-map-sq, top wf, decidable equal Id, index wf, int seg wf, length wf1, rcv-from-on wf, receives wf, idlnk-deq wf, rcv?-kind, rel exp wf, nat plus inc, haslink wf, Msg wf, isrcv wf, iff wf, squash wf, true wf, lnk wf, kind wf, iff functionality wrt iff, nat wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, Id sq, subtype rel self, event system wf, SES-implies-ES, kindcase wf, Knd wf, pi2 wf, ldst wf, unit wf, strongwellfounded wf, pred! wf, lsrc wf, rcv? wf, IdLnk wf, link wf, sender wf, cless wf, not wf, assert wf, first wf, when-after wf, pred wf, pi1 wf, loc wf, Id wf